$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$), $e$:E. ($\uparrow$($e$ $\in_{b}$ $X$)) $\Rightarrow$ ($X$($e$) $\in$ $A$)